Inference at * 1 1 
Iof proof for Lemma integer sqrt:

.....basecase..... NILNIL

  r:. (((r * r)  0) & (0 < ((r+1) * (r+1)))) 

latex

 by With 0 (D 0) THEN Auto 

latex

 .

Definitions	#$n, x:A. B(x), Type, A, False, P  Q, Void, P & Q, x:A  B(x), A  B, x:A. B(x), x:AB(x), s = t, S  T, |g|, , , {x:A| B(x)} , , a < b, n * m, n+m, t  T
Lemmas	nat wf, member wf, le wf